WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) minSort(l) -> minSort#1(findMin(l)) minSort#1(dd(x,xs)) -> dd(x,minSort(xs)) minSort#1(nil()) -> nil() - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt,#compare,#less,findMin,findMin#1,findMin#2 ,findMin#3,minSort,minSort#1} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #cklt#(#EQ()) -> c_1() #cklt#(#GT()) -> c_2() #cklt#(#LT()) -> c_3() #compare#(#0(),#0()) -> c_4() #compare#(#0(),#neg(y)) -> c_5() #compare#(#0(),#pos(y)) -> c_6() #compare#(#0(),#s(y)) -> c_7() #compare#(#neg(x),#0()) -> c_8() #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#neg(x),#pos(y)) -> c_10() #compare#(#pos(x),#0()) -> c_11() #compare#(#pos(x),#neg(y)) -> c_12() #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#0()) -> c_14() #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#1#(nil()) -> c_19() findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)) findMin#2#(nil(),x) -> c_21() findMin#3#(#false(),x,y,ys) -> c_22() findMin#3#(#true(),x,y,ys) -> c_23() minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) minSort#1#(nil()) -> c_26() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #cklt#(#EQ()) -> c_1() #cklt#(#GT()) -> c_2() #cklt#(#LT()) -> c_3() #compare#(#0(),#0()) -> c_4() #compare#(#0(),#neg(y)) -> c_5() #compare#(#0(),#pos(y)) -> c_6() #compare#(#0(),#s(y)) -> c_7() #compare#(#neg(x),#0()) -> c_8() #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#neg(x),#pos(y)) -> c_10() #compare#(#pos(x),#0()) -> c_11() #compare#(#pos(x),#neg(y)) -> c_12() #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#0()) -> c_14() #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#1#(nil()) -> c_19() findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)) findMin#2#(nil(),x) -> c_21() findMin#3#(#false(),x,y,ys) -> c_22() findMin#3#(#true(),x,y,ys) -> c_23() minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) minSort#1#(nil()) -> c_26() - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) minSort(l) -> minSort#1(findMin(l)) minSort#1(dd(x,xs)) -> dd(x,minSort(xs)) minSort#1(nil()) -> nil() - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5,6,7,8,10,11,12,14,19,21,22,23,26} by application of Pre({1,2,3,4,5,6,7,8,10,11,12,14,19,21,22,23,26}) = {9,13,15,16,17,18,20,24}. Here rules are labelled as follows: 1: #cklt#(#EQ()) -> c_1() 2: #cklt#(#GT()) -> c_2() 3: #cklt#(#LT()) -> c_3() 4: #compare#(#0(),#0()) -> c_4() 5: #compare#(#0(),#neg(y)) -> c_5() 6: #compare#(#0(),#pos(y)) -> c_6() 7: #compare#(#0(),#s(y)) -> c_7() 8: #compare#(#neg(x),#0()) -> c_8() 9: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) 10: #compare#(#neg(x),#pos(y)) -> c_10() 11: #compare#(#pos(x),#0()) -> c_11() 12: #compare#(#pos(x),#neg(y)) -> c_12() 13: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) 14: #compare#(#s(x),#0()) -> c_14() 15: #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) 16: #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)) 17: findMin#(l) -> c_17(findMin#1#(l)) 18: findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) 19: findMin#1#(nil()) -> c_19() 20: findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)) 21: findMin#2#(nil(),x) -> c_21() 22: findMin#3#(#false(),x,y,ys) -> c_22() 23: findMin#3#(#true(),x,y,ys) -> c_23() 24: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) 25: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) 26: minSort#1#(nil()) -> c_26() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)) minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) - Weak DPs: #cklt#(#EQ()) -> c_1() #cklt#(#GT()) -> c_2() #cklt#(#LT()) -> c_3() #compare#(#0(),#0()) -> c_4() #compare#(#0(),#neg(y)) -> c_5() #compare#(#0(),#pos(y)) -> c_6() #compare#(#0(),#s(y)) -> c_7() #compare#(#neg(x),#0()) -> c_8() #compare#(#neg(x),#pos(y)) -> c_10() #compare#(#pos(x),#0()) -> c_11() #compare#(#pos(x),#neg(y)) -> c_12() #compare#(#s(x),#0()) -> c_14() findMin#1#(nil()) -> c_19() findMin#2#(nil(),x) -> c_21() findMin#3#(#false(),x,y,ys) -> c_22() findMin#3#(#true(),x,y,ys) -> c_23() minSort#1#(nil()) -> c_26() - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) minSort(l) -> minSort#1(findMin(l)) minSort#1(dd(x,xs)) -> dd(x,minSort(xs)) minSort#1(nil()) -> nil() - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) -->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2 -->_1 #compare#(#s(x),#0()) -> c_14():21 -->_1 #compare#(#pos(x),#neg(y)) -> c_12():20 -->_1 #compare#(#pos(x),#0()) -> c_11():19 -->_1 #compare#(#neg(x),#pos(y)) -> c_10():18 -->_1 #compare#(#neg(x),#0()) -> c_8():17 -->_1 #compare#(#0(),#s(y)) -> c_7():16 -->_1 #compare#(#0(),#pos(y)) -> c_6():15 -->_1 #compare#(#0(),#neg(y)) -> c_5():14 -->_1 #compare#(#0(),#0()) -> c_4():13 -->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1 2:S:#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) -->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3 -->_1 #compare#(#s(x),#0()) -> c_14():21 -->_1 #compare#(#pos(x),#neg(y)) -> c_12():20 -->_1 #compare#(#pos(x),#0()) -> c_11():19 -->_1 #compare#(#neg(x),#pos(y)) -> c_10():18 -->_1 #compare#(#neg(x),#0()) -> c_8():17 -->_1 #compare#(#0(),#s(y)) -> c_7():16 -->_1 #compare#(#0(),#pos(y)) -> c_6():15 -->_1 #compare#(#0(),#neg(y)) -> c_5():14 -->_1 #compare#(#0(),#0()) -> c_4():13 -->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1 3:S:#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) -->_1 #compare#(#s(x),#0()) -> c_14():21 -->_1 #compare#(#pos(x),#neg(y)) -> c_12():20 -->_1 #compare#(#pos(x),#0()) -> c_11():19 -->_1 #compare#(#neg(x),#pos(y)) -> c_10():18 -->_1 #compare#(#neg(x),#0()) -> c_8():17 -->_1 #compare#(#0(),#s(y)) -> c_7():16 -->_1 #compare#(#0(),#pos(y)) -> c_6():15 -->_1 #compare#(#0(),#neg(y)) -> c_5():14 -->_1 #compare#(#0(),#0()) -> c_4():13 -->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1 4:S:#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)) -->_2 #compare#(#s(x),#0()) -> c_14():21 -->_2 #compare#(#pos(x),#neg(y)) -> c_12():20 -->_2 #compare#(#pos(x),#0()) -> c_11():19 -->_2 #compare#(#neg(x),#pos(y)) -> c_10():18 -->_2 #compare#(#neg(x),#0()) -> c_8():17 -->_2 #compare#(#0(),#s(y)) -> c_7():16 -->_2 #compare#(#0(),#pos(y)) -> c_6():15 -->_2 #compare#(#0(),#neg(y)) -> c_5():14 -->_2 #compare#(#0(),#0()) -> c_4():13 -->_1 #cklt#(#LT()) -> c_3():12 -->_1 #cklt#(#GT()) -> c_2():11 -->_1 #cklt#(#EQ()) -> c_1():10 -->_2 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3 -->_2 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2 -->_2 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1 5:S:findMin#(l) -> c_17(findMin#1#(l)) -->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)):6 -->_1 findMin#1#(nil()) -> c_19():22 6:S:findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) -->_1 findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)):7 -->_1 findMin#2#(nil(),x) -> c_21():23 -->_2 findMin#(l) -> c_17(findMin#1#(l)):5 7:S:findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)) -->_1 findMin#3#(#true(),x,y,ys) -> c_23():25 -->_1 findMin#3#(#false(),x,y,ys) -> c_22():24 -->_2 #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)):4 8:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) -->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):9 -->_1 minSort#1#(nil()) -> c_26():26 -->_2 findMin#(l) -> c_17(findMin#1#(l)):5 9:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) -->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):8 10:W:#cklt#(#EQ()) -> c_1() 11:W:#cklt#(#GT()) -> c_2() 12:W:#cklt#(#LT()) -> c_3() 13:W:#compare#(#0(),#0()) -> c_4() 14:W:#compare#(#0(),#neg(y)) -> c_5() 15:W:#compare#(#0(),#pos(y)) -> c_6() 16:W:#compare#(#0(),#s(y)) -> c_7() 17:W:#compare#(#neg(x),#0()) -> c_8() 18:W:#compare#(#neg(x),#pos(y)) -> c_10() 19:W:#compare#(#pos(x),#0()) -> c_11() 20:W:#compare#(#pos(x),#neg(y)) -> c_12() 21:W:#compare#(#s(x),#0()) -> c_14() 22:W:findMin#1#(nil()) -> c_19() 23:W:findMin#2#(nil(),x) -> c_21() 24:W:findMin#3#(#false(),x,y,ys) -> c_22() 25:W:findMin#3#(#true(),x,y,ys) -> c_23() 26:W:minSort#1#(nil()) -> c_26() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 26: minSort#1#(nil()) -> c_26() 22: findMin#1#(nil()) -> c_19() 23: findMin#2#(nil(),x) -> c_21() 24: findMin#3#(#false(),x,y,ys) -> c_22() 25: findMin#3#(#true(),x,y,ys) -> c_23() 10: #cklt#(#EQ()) -> c_1() 11: #cklt#(#GT()) -> c_2() 12: #cklt#(#LT()) -> c_3() 13: #compare#(#0(),#0()) -> c_4() 14: #compare#(#0(),#neg(y)) -> c_5() 15: #compare#(#0(),#pos(y)) -> c_6() 16: #compare#(#0(),#s(y)) -> c_7() 17: #compare#(#neg(x),#0()) -> c_8() 18: #compare#(#neg(x),#pos(y)) -> c_10() 19: #compare#(#pos(x),#0()) -> c_11() 20: #compare#(#pos(x),#neg(y)) -> c_12() 21: #compare#(#s(x),#0()) -> c_14() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)) minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) minSort(l) -> minSort#1(findMin(l)) minSort#1(dd(x,xs)) -> dd(x,minSort(xs)) minSort#1(nil()) -> nil() - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) -->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1 2:S:#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) -->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1 3:S:#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) -->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3 -->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2 -->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1 4:S:#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)) -->_2 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3 -->_2 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2 -->_2 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1 5:S:findMin#(l) -> c_17(findMin#1#(l)) -->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)):6 6:S:findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) -->_1 findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)):7 -->_2 findMin#(l) -> c_17(findMin#1#(l)):5 7:S:findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)) -->_2 #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)):4 8:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) -->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):9 -->_2 findMin#(l) -> c_17(findMin#1#(l)):5 9:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) -->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):8 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: #less#(x,y) -> c_16(#compare#(x,y)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) minSort(l) -> minSort#1(findMin(l)) minSort#1(dd(x,xs)) -> dd(x,minSort(xs)) minSort#1(nil()) -> nil() - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) and a lower component #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) Further, following extension rules are added to the lower component. minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)) -->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):2 2:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) -->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: minSort#(l) -> c_24(minSort#1#(findMin(l))) ** Step 6.a:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: minSort#(l) -> c_24(minSort#1#(findMin(l))) minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(14) #GT :: [] -(0)-> "A"(10) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(14) #cklt :: ["A"(0)] -(0)-> "A"(0) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(14) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(12) dd :: ["A"(0) x "A"(7)] -(7)-> "A"(7) findMin :: ["A"(7)] -(0)-> "A"(7) findMin#1 :: ["A"(7)] -(0)-> "A"(7) findMin#2 :: ["A"(7) x "A"(0)] -(7)-> "A"(7) findMin#3 :: ["A"(0) x "A"(0) x "A"(0) x "A"(7)] -(14)-> "A"(7) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(15) minSort# :: ["A"(7)] -(4)-> "A"(0) minSort#1# :: ["A"(7)] -(0)-> "A"(14) c_24 :: ["A"(0)] -(3)-> "A"(3) c_25 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(0)] -(0)-> "A"(1) "#pos_A" :: ["A"(0)] -(0)-> "A"(1) "#s_A" :: ["A"(0)] -(0)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_24_A" :: ["A"(0)] -(1)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) 2. Weak: minSort#(l) -> c_24(minSort#1#(findMin(l))) ** Step 6.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: minSort#(l) -> c_24(minSort#1#(findMin(l))) - Weak DPs: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(14) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(14) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(14) #cklt :: ["A"(0)] -(0)-> "A"(0) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(14) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(14) dd :: ["A"(0) x "A"(7)] -(7)-> "A"(7) findMin :: ["A"(7)] -(1)-> "A"(7) findMin#1 :: ["A"(7)] -(1)-> "A"(7) findMin#2 :: ["A"(7) x "A"(0)] -(7)-> "A"(7) findMin#3 :: ["A"(0) x "A"(0) x "A"(0) x "A"(7)] -(14)-> "A"(7) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(8) nil :: [] -(0)-> "A"(15) minSort# :: ["A"(7)] -(10)-> "A"(0) minSort#1# :: ["A"(7)] -(3)-> "A"(12) c_24 :: ["A"(0)] -(0)-> "A"(14) c_25 :: ["A"(0)] -(0)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(0)] -(0)-> "A"(1) "#pos_A" :: ["A"(0)] -(0)-> "A"(1) "#s_A" :: ["A"(0)] -(0)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_24_A" :: ["A"(0)] -(0)-> "A"(1) "c_25_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: minSort#(l) -> c_24(minSort#1#(findMin(l))) 2. Weak: ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) - Weak DPs: minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) and a lower component #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) Further, following extension rules are added to the lower component. findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) *** Step 6.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) - Weak DPs: minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:findMin#(l) -> c_17(findMin#1#(l)) -->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)):2 2:S:findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) -->_2 findMin#(l) -> c_17(findMin#1#(l)):1 3:W:minSort#(l) -> findMin#(l) -->_1 findMin#(l) -> c_17(findMin#1#(l)):1 4:W:minSort#(l) -> minSort#1#(findMin(l)) -->_1 minSort#1#(dd(x,xs)) -> minSort#(xs):5 5:W:minSort#1#(dd(x,xs)) -> minSort#(xs) -->_1 minSort#(l) -> minSort#1#(findMin(l)):4 -->_1 minSort#(l) -> findMin#(l):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: findMin#1#(dd(x,xs)) -> c_18(findMin#(xs)) *** Step 6.b:1.a:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#(xs)) - Weak DPs: minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(15) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(15) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(15) #cklt :: ["A"(0)] -(0)-> "A"(9) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(15) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(15) dd :: ["A"(0) x "A"(7)] -(7)-> "A"(7) findMin :: ["A"(7)] -(0)-> "A"(7) findMin#1 :: ["A"(7)] -(0)-> "A"(7) findMin#2 :: ["A"(7) x "A"(0)] -(7)-> "A"(7) findMin#3 :: ["A"(0) x "A"(0) x "A"(0) x "A"(7)] -(14)-> "A"(7) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(15) findMin# :: ["A"(7)] -(2)-> "A"(1) findMin#1# :: ["A"(7)] -(0)-> "A"(12) minSort# :: ["A"(7)] -(8)-> "A"(0) minSort#1# :: ["A"(7)] -(1)-> "A"(0) c_17 :: ["A"(0)] -(0)-> "A"(12) c_18 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(0)] -(1)-> "A"(1) "#pos_A" :: ["A"(0)] -(0)-> "A"(1) "#s_A" :: ["A"(0)] -(1)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_17_A" :: ["A"(0)] -(0)-> "A"(1) "c_18_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: findMin#1#(dd(x,xs)) -> c_18(findMin#(xs)) 2. Weak: findMin#(l) -> c_17(findMin#1#(l)) *** Step 6.b:1.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: findMin#(l) -> c_17(findMin#1#(l)) - Weak DPs: findMin#1#(dd(x,xs)) -> c_18(findMin#(xs)) minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(6) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(14) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(14) #cklt :: ["A"(0)] -(0)-> "A"(0) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(14) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(14) dd :: ["A"(6) x "A"(6)] -(6)-> "A"(6) findMin :: ["A"(6)] -(0)-> "A"(6) findMin#1 :: ["A"(6)] -(0)-> "A"(6) findMin#2 :: ["A"(6) x "A"(6)] -(6)-> "A"(6) findMin#3 :: ["A"(0) x "A"(6) x "A"(6) x "A"(6)] -(12)-> "A"(6) nil :: [] -(0)-> "A"(6) nil :: [] -(0)-> "A"(14) findMin# :: ["A"(6)] -(12)-> "A"(0) findMin#1# :: ["A"(6)] -(7)-> "A"(0) minSort# :: ["A"(6)] -(14)-> "A"(0) minSort#1# :: ["A"(6)] -(8)-> "A"(0) c_17 :: ["A"(0)] -(0)-> "A"(14) c_18 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(0)] -(0)-> "A"(1) "#pos_A" :: ["A"(0)] -(0)-> "A"(1) "#s_A" :: ["A"(0)] -(0)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_17_A" :: ["A"(0)] -(0)-> "A"(1) "c_18_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: findMin#(l) -> c_17(findMin#1#(l)) 2. Weak: *** Step 6.b:1.b:1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) - Weak DPs: findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(0) #cklt :: ["A"(0)] -(0)-> "A"(0) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #false :: [] -(0)-> "A"(0) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) findMin :: ["A"(0)] -(0)-> "A"(0) findMin#1 :: ["A"(0)] -(0)-> "A"(0) findMin#2 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) findMin#3 :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) nil :: [] -(0)-> "A"(0) #compare# :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #less# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) findMin# :: ["A"(0)] -(2)-> "A"(0) findMin#1# :: ["A"(0)] -(2)-> "A"(0) findMin#2# :: ["A"(0) x "A"(0)] -(2)-> "A"(0) minSort# :: ["A"(0)] -(2)-> "A"(0) minSort#1# :: ["A"(0)] -(2)-> "A"(0) c_9 :: ["A"(0)] -(0)-> "A"(0) c_13 :: ["A"(0)] -(0)-> "A"(0) c_15 :: ["A"(0)] -(0)-> "A"(0) c_16 :: ["A"(0)] -(0)-> "A"(0) c_20 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: #less#(x,y) -> c_16(#compare#(x,y)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) 2. Weak: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) *** Step 6.b:1.b:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) - Weak DPs: #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(15) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(15) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(15) #cklt :: ["A"(0)] -(0)-> "A"(9) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(15) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(9) #neg :: ["A"(8)] -(0)-> "A"(8) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(8)] -(8)-> "A"(8) #pos :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(8)] -(8)-> "A"(8) #s :: ["A"(0)] -(0)-> "A"(0) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(15) dd :: ["A"(13) x "A"(13)] -(0)-> "A"(13) dd :: ["A"(9) x "A"(9)] -(0)-> "A"(9) findMin :: ["A"(13)] -(0)-> "A"(13) findMin#1 :: ["A"(13)] -(0)-> "A"(13) findMin#2 :: ["A"(13) x "A"(13)] -(0)-> "A"(13) findMin#3 :: ["A"(0) x "A"(13) x "A"(13) x "A"(13)] -(0)-> "A"(13) nil :: [] -(0)-> "A"(13) nil :: [] -(0)-> "A"(15) #compare# :: ["A"(8) x "A"(8)] -(8)-> "A"(1) #less# :: ["A"(9) x "A"(9)] -(8)-> "A"(1) findMin# :: ["A"(13)] -(9)-> "A"(14) findMin#1# :: ["A"(13)] -(9)-> "A"(14) findMin#2# :: ["A"(9) x "A"(9)] -(8)-> "A"(15) minSort# :: ["A"(13)] -(9)-> "A"(7) minSort#1# :: ["A"(13)] -(9)-> "A"(7) c_9 :: ["A"(0)] -(0)-> "A"(12) c_13 :: ["A"(0)] -(0)-> "A"(12) c_15 :: ["A"(0)] -(1)-> "A"(1) c_16 :: ["A"(0)] -(0)-> "A"(12) c_20 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(1)] -(0)-> "A"(1) "#pos_A" :: ["A"(1)] -(1)-> "A"(1) "#s_A" :: ["A"(1)] -(1)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_13_A" :: ["A"(0)] -(0)-> "A"(1) "c_15_A" :: ["A"(0)] -(1)-> "A"(1) "c_16_A" :: ["A"(0)] -(0)-> "A"(1) "c_20_A" :: ["A"(0)] -(0)-> "A"(1) "c_9_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) 2. Weak: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) *** Step 6.b:1.b:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) - Weak DPs: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(y)) -> #GT() #compare(#0(),#pos(y)) -> #LT() #compare(#0(),#s(y)) -> #LT() #compare(#neg(x),#0()) -> #LT() #compare(#neg(x),#neg(y)) -> #compare(y,x) #compare(#neg(x),#pos(y)) -> #LT() #compare(#pos(x),#0()) -> #GT() #compare(#pos(x),#neg(y)) -> #GT() #compare(#pos(x),#pos(y)) -> #compare(x,y) #compare(#s(x),#0()) -> #GT() #compare(#s(x),#s(y)) -> #compare(x,y) #less(x,y) -> #cklt(#compare(x,y)) findMin(l) -> findMin#1(l) findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x) findMin#1(nil()) -> nil() findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) -> dd(x,nil()) findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys)) - Signature: {#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1 ,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0 ,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/2,c_25/1,c_26/0} - Obligation: innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2# ,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(0) #EQ :: [] -(0)-> "A"(14) #GT :: [] -(0)-> "A"(0) #GT :: [] -(0)-> "A"(14) #LT :: [] -(0)-> "A"(0) #LT :: [] -(0)-> "A"(14) #LT :: [] -(0)-> "A"(6) #cklt :: ["A"(0)] -(0)-> "A"(0) #compare :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #false :: [] -(0)-> "A"(0) #false :: [] -(0)-> "A"(14) #less :: ["A"(0) x "A"(0)] -(0)-> "A"(0) #neg :: ["A"(2)] -(2)-> "A"(2) #neg :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(0)] -(0)-> "A"(0) #pos :: ["A"(2)] -(2)-> "A"(2) #s :: ["A"(0)] -(0)-> "A"(0) #s :: ["A"(2)] -(2)-> "A"(2) #true :: [] -(0)-> "A"(0) #true :: [] -(0)-> "A"(14) dd :: ["A"(3) x "A"(3)] -(3)-> "A"(3) findMin :: ["A"(3)] -(1)-> "A"(3) findMin#1 :: ["A"(3)] -(1)-> "A"(3) findMin#2 :: ["A"(3) x "A"(3)] -(3)-> "A"(3) findMin#3 :: ["A"(0) x "A"(3) x "A"(3) x "A"(3)] -(6)-> "A"(3) nil :: [] -(0)-> "A"(3) nil :: [] -(0)-> "A"(15) #compare# :: ["A"(2) x "A"(2)] -(14)-> "A"(0) #less# :: ["A"(2) x "A"(2)] -(15)-> "A"(0) findMin# :: ["A"(3)] -(11)-> "A"(8) findMin#1# :: ["A"(3)] -(11)-> "A"(8) findMin#2# :: ["A"(3) x "A"(2)] -(12)-> "A"(8) minSort# :: ["A"(3)] -(12)-> "A"(0) minSort#1# :: ["A"(3)] -(11)-> "A"(0) c_9 :: ["A"(0)] -(0)-> "A"(14) c_13 :: ["A"(0)] -(0)-> "A"(14) c_15 :: ["A"(0)] -(0)-> "A"(0) c_16 :: ["A"(0)] -(0)-> "A"(14) c_20 :: ["A"(0)] -(0)-> "A"(8) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: [] -(0)-> "A"(1) "#EQ_A" :: [] -(0)-> "A"(1) "#GT_A" :: [] -(0)-> "A"(1) "#LT_A" :: [] -(0)-> "A"(1) "#false_A" :: [] -(0)-> "A"(1) "#neg_A" :: ["A"(1)] -(1)-> "A"(1) "#pos_A" :: ["A"(1)] -(1)-> "A"(1) "#s_A" :: ["A"(1)] -(1)-> "A"(1) "#true_A" :: [] -(0)-> "A"(1) "c_13_A" :: ["A"(0)] -(0)-> "A"(1) "c_15_A" :: ["A"(0)] -(0)-> "A"(1) "c_16_A" :: ["A"(0)] -(0)-> "A"(1) "c_20_A" :: ["A"(0)] -(0)-> "A"(1) "c_9_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) 2. Weak: WORST_CASE(?,O(n^3))